from cheqed.core.sexp import sexp, unary_op, binary_op, sexp_to_string

class Formula(object):
    def __str__(self):
        return sexp_to_string(self.sexp())

    def __getitem__(self, key):
        return self.args[key]

    def __repr__(self):
        return str(self)

class Relation(Formula):
    operator = "relation"
    
    def __init__(self, name, *args):
        self.name = name
        self.args = args

    def sexp(self):
        if len(self.args) == 0:
            return self.name
        else:
            return [self.name] + [sexp(arg) for arg in self.args]
    
    def __eq__(self, other):
        return (self.operator == other.operator
                and self.name == other.name
                and self.args == other.args)

    def free_variables(self):
        return reduce(lambda x, y: x.union(y),
                      [ arg.free_variables() for arg in self.args ])

    def substitute(self, a, b):
        return Relation(self.name,
                        *[term.substitute(a, b) for term in self.args])
            
class Operator(Formula):
    def __eq__(self, other):
        return self.operator == other.operator \
               and self.args == other.args

    def free_variables(self):
        return reduce(lambda x, y: x.union(y),
                      [form.free_variables() for form in self.args])

    def substitute(self, a, b):
        return self.__class__(*[form.substitute(a, b) for form in self.args])
    
class UnaryOp(Operator):
    def sexp(self):
        return unary_op(self.operator, self.args[0])

class BinaryOp(Operator):
    def sexp(self):
        return binary_op(self.operator, self.args[0], self.args[1])
        
class Negation(UnaryOp):
    operator = "not"
    
    def __init__(self, *args):
        self.args = args

class Disjunction(BinaryOp):
    operator = "or"
    
    def __init__(self, *args):
        self.args = args

class Conjunction(BinaryOp):
    operator = "and"
    
    def __init__(self, *args):
        self.args = args

class Conditional(BinaryOp):
    operator = "if"
    
    def __init__(self, *args):
        self.args = args

class Biconditional(BinaryOp):
    operator = "iff"
    
    def __init__(self, *args):
        self.args = args

class SubstitutionError(Exception):
    pass

class Quantifier(BinaryOp):
    @property
    def bound(self):
        return self.args[0]

    @property
    def formula(self):
        return self.args[1]

    def free_variables(self):
        return self.args[1].free_variables().difference(set([ self.args[0] ]))

    def substitute(self, a, b):
        if b.free_variables().issubset(self.free_variables()):
            if self.args[0] in a.free_variables():
                raise SubstitutionError()

            return self.__class__(self.args[0],
                                  self.args[1].substitute(a, b))

        return self

class Universal(Quantifier):
    operator = "for_all"

    def __init__(self, *args):
        self.args = args

class Existential(Quantifier):
    operator = "exists"

    def __init__(self, *args):
        self.args = args
